(0) Obligation:
Clauses:
star(U, []) :- !.
star([], W) :- ','(!, =(W, [])).
star(U, W) :- ','(app(U, V, W), star(U, V)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).
=(X, X).
Query: star(g,g)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
star(U, []) :- !.
star([], W) :- ','(!, user_defined_=(W, [])).
star(U, W) :- ','(app(U, V, W), star(U, V)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).
user_defined_=(X, X).
Query: star(g,g)
(3) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(4) Obligation:
Triples:
appB(.(X1, X2), X3, .(X1, X4)) :- appB(X2, X3, X4).
starA(.(X1, X2), .(X1, X3)) :- appB(X2, X4, X3).
starA(.(X1, X2), .(X1, X3)) :- ','(appcB(X2, X4, X3), starA(.(X1, X2), X4)).
Clauses:
starcA(X1, []).
starcA(.(X1, X2), .(X1, X3)) :- ','(appcB(X2, X4, X3), starcA(.(X1, X2), X4)).
appcB([], X1, X1).
appcB(.(X1, X2), X3, .(X1, X4)) :- appcB(X2, X3, X4).
Afs:
starA(x1, x2) = starA(x1, x2)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
starA_in: (b,b)
appB_in: (b,f,b)
appcB_in: (b,f,b)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U2_GG(X1, X2, X3, appB_in_gag(X2, X4, X3))
STARA_IN_GG(.(X1, X2), .(X1, X3)) → APPB_IN_GAG(X2, X4, X3)
APPB_IN_GAG(.(X1, X2), X3, .(X1, X4)) → U1_GAG(X1, X2, X3, X4, appB_in_gag(X2, X3, X4))
APPB_IN_GAG(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GAG(X2, X3, X4)
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U3_GG(X1, X2, X3, appcB_in_gag(X2, X4, X3))
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → U4_GG(X1, X2, X3, starA_in_gg(.(X1, X2), X4))
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → STARA_IN_GG(.(X1, X2), X4)
The TRS R consists of the following rules:
appcB_in_gag([], X1, X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), X3, .(X1, X4)) → U8_gag(X1, X2, X3, X4, appcB_in_gag(X2, X3, X4))
U8_gag(X1, X2, X3, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
The argument filtering Pi contains the following mapping:
starA_in_gg(
x1,
x2) =
starA_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
appB_in_gag(
x1,
x2,
x3) =
appB_in_gag(
x1,
x3)
appcB_in_gag(
x1,
x2,
x3) =
appcB_in_gag(
x1,
x3)
[] =
[]
appcB_out_gag(
x1,
x2,
x3) =
appcB_out_gag(
x1,
x2,
x3)
U8_gag(
x1,
x2,
x3,
x4,
x5) =
U8_gag(
x1,
x2,
x4,
x5)
STARA_IN_GG(
x1,
x2) =
STARA_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3,
x4) =
U2_GG(
x1,
x2,
x3,
x4)
APPB_IN_GAG(
x1,
x2,
x3) =
APPB_IN_GAG(
x1,
x3)
U1_GAG(
x1,
x2,
x3,
x4,
x5) =
U1_GAG(
x1,
x2,
x4,
x5)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x1,
x2,
x3,
x4)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U2_GG(X1, X2, X3, appB_in_gag(X2, X4, X3))
STARA_IN_GG(.(X1, X2), .(X1, X3)) → APPB_IN_GAG(X2, X4, X3)
APPB_IN_GAG(.(X1, X2), X3, .(X1, X4)) → U1_GAG(X1, X2, X3, X4, appB_in_gag(X2, X3, X4))
APPB_IN_GAG(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GAG(X2, X3, X4)
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U3_GG(X1, X2, X3, appcB_in_gag(X2, X4, X3))
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → U4_GG(X1, X2, X3, starA_in_gg(.(X1, X2), X4))
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → STARA_IN_GG(.(X1, X2), X4)
The TRS R consists of the following rules:
appcB_in_gag([], X1, X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), X3, .(X1, X4)) → U8_gag(X1, X2, X3, X4, appcB_in_gag(X2, X3, X4))
U8_gag(X1, X2, X3, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
The argument filtering Pi contains the following mapping:
starA_in_gg(
x1,
x2) =
starA_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
appB_in_gag(
x1,
x2,
x3) =
appB_in_gag(
x1,
x3)
appcB_in_gag(
x1,
x2,
x3) =
appcB_in_gag(
x1,
x3)
[] =
[]
appcB_out_gag(
x1,
x2,
x3) =
appcB_out_gag(
x1,
x2,
x3)
U8_gag(
x1,
x2,
x3,
x4,
x5) =
U8_gag(
x1,
x2,
x4,
x5)
STARA_IN_GG(
x1,
x2) =
STARA_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3,
x4) =
U2_GG(
x1,
x2,
x3,
x4)
APPB_IN_GAG(
x1,
x2,
x3) =
APPB_IN_GAG(
x1,
x3)
U1_GAG(
x1,
x2,
x3,
x4,
x5) =
U1_GAG(
x1,
x2,
x4,
x5)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x1,
x2,
x3,
x4)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPB_IN_GAG(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GAG(X2, X3, X4)
The TRS R consists of the following rules:
appcB_in_gag([], X1, X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), X3, .(X1, X4)) → U8_gag(X1, X2, X3, X4, appcB_in_gag(X2, X3, X4))
U8_gag(X1, X2, X3, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcB_in_gag(
x1,
x2,
x3) =
appcB_in_gag(
x1,
x3)
[] =
[]
appcB_out_gag(
x1,
x2,
x3) =
appcB_out_gag(
x1,
x2,
x3)
U8_gag(
x1,
x2,
x3,
x4,
x5) =
U8_gag(
x1,
x2,
x4,
x5)
APPB_IN_GAG(
x1,
x2,
x3) =
APPB_IN_GAG(
x1,
x3)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPB_IN_GAG(.(X1, X2), X3, .(X1, X4)) → APPB_IN_GAG(X2, X3, X4)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPB_IN_GAG(
x1,
x2,
x3) =
APPB_IN_GAG(
x1,
x3)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPB_IN_GAG(.(X1, X2), .(X1, X4)) → APPB_IN_GAG(X2, X4)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- APPB_IN_GAG(.(X1, X2), .(X1, X4)) → APPB_IN_GAG(X2, X4)
The graph contains the following edges 1 > 1, 2 > 2
(15) YES
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U3_GG(X1, X2, X3, appcB_in_gag(X2, X4, X3))
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → STARA_IN_GG(.(X1, X2), X4)
The TRS R consists of the following rules:
appcB_in_gag([], X1, X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), X3, .(X1, X4)) → U8_gag(X1, X2, X3, X4, appcB_in_gag(X2, X3, X4))
U8_gag(X1, X2, X3, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
appcB_in_gag(
x1,
x2,
x3) =
appcB_in_gag(
x1,
x3)
[] =
[]
appcB_out_gag(
x1,
x2,
x3) =
appcB_out_gag(
x1,
x2,
x3)
U8_gag(
x1,
x2,
x3,
x4,
x5) =
U8_gag(
x1,
x2,
x4,
x5)
STARA_IN_GG(
x1,
x2) =
STARA_IN_GG(
x1,
x2)
U3_GG(
x1,
x2,
x3,
x4) =
U3_GG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U3_GG(X1, X2, X3, appcB_in_gag(X2, X3))
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → STARA_IN_GG(.(X1, X2), X4)
The TRS R consists of the following rules:
appcB_in_gag([], X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), .(X1, X4)) → U8_gag(X1, X2, X4, appcB_in_gag(X2, X4))
U8_gag(X1, X2, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
The set Q consists of the following terms:
appcB_in_gag(x0, x1)
U8_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(19) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
STARA_IN_GG(.(X1, X2), .(X1, X3)) → U3_GG(X1, X2, X3, appcB_in_gag(X2, X3))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(.(x1, x2)) = 1 + x2
POL(STARA_IN_GG(x1, x2)) = x1 + x2
POL(U3_GG(x1, x2, x3, x4)) = 1 + x4
POL(U8_gag(x1, x2, x3, x4)) = 1 + x4
POL([]) = 0
POL(appcB_in_gag(x1, x2)) = x2
POL(appcB_out_gag(x1, x2, x3)) = x1 + x2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
appcB_in_gag([], X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), .(X1, X4)) → U8_gag(X1, X2, X4, appcB_in_gag(X2, X4))
U8_gag(X1, X2, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GG(X1, X2, X3, appcB_out_gag(X2, X4, X3)) → STARA_IN_GG(.(X1, X2), X4)
The TRS R consists of the following rules:
appcB_in_gag([], X1) → appcB_out_gag([], X1, X1)
appcB_in_gag(.(X1, X2), .(X1, X4)) → U8_gag(X1, X2, X4, appcB_in_gag(X2, X4))
U8_gag(X1, X2, X4, appcB_out_gag(X2, X3, X4)) → appcB_out_gag(.(X1, X2), X3, .(X1, X4))
The set Q consists of the following terms:
appcB_in_gag(x0, x1)
U8_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(22) TRUE